Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
Q is empty.
↳ QTRS
↳ Overlay + Local Confluence
Q restricted rewrite system:
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
Q is empty.
The TRS is overlay and locally confluent. By [19] we can switch to innermost.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, l) → TAIL(l)
IF(false, x, l) → HEAD(l)
REV(cons(x, l)) → REV2(x, l)
IF(false, x, l) → LAST(head(l), tail(l))
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
LAST(x, l) → EMPTY(l)
LAST(x, l) → IF(empty(l), x, l)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, l) → TAIL(l)
IF(false, x, l) → HEAD(l)
REV(cons(x, l)) → REV2(x, l)
IF(false, x, l) → LAST(head(l), tail(l))
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
LAST(x, l) → EMPTY(l)
LAST(x, l) → IF(empty(l), x, l)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 3 less nodes.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil) → true
empty(cons(x, l)) → false
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil) → true
empty(cons(x, l)) → false
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule LAST(x, l) → IF(empty(l), x, l) at position [0] we obtained the following new rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
LAST(y0, nil) → IF(true, y0, nil)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, x, l) → LAST(head(l), tail(l))
LAST(y0, nil) → IF(true, y0, nil)
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil) → true
empty(cons(x, l)) → false
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, x, l) → LAST(head(l), tail(l))
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil) → true
empty(cons(x, l)) → false
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, x, l) → LAST(head(l), tail(l))
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
empty(nil)
empty(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, x, l) → LAST(head(l), tail(l))
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
The set Q consists of the following terms:
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule IF(false, x, l) → LAST(head(l), tail(l)) at position [1] we obtained the following new rules:
IF(false, y0, cons(x0, x1)) → LAST(head(cons(x0, x1)), x1)
IF(false, y0, nil) → LAST(head(nil), nil)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, nil) → LAST(head(nil), nil)
IF(false, y0, cons(x0, x1)) → LAST(head(cons(x0, x1)), x1)
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
The set Q consists of the following terms:
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, cons(x0, x1)) → LAST(head(cons(x0, x1)), x1)
The TRS R consists of the following rules:
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
The set Q consists of the following terms:
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, cons(x0, x1)) → LAST(head(cons(x0, x1)), x1)
The TRS R consists of the following rules:
head(cons(x, l)) → x
The set Q consists of the following terms:
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
tail(nil)
tail(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, cons(x0, x1)) → LAST(head(cons(x0, x1)), x1)
The TRS R consists of the following rules:
head(cons(x, l)) → x
The set Q consists of the following terms:
head(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule IF(false, y0, cons(x0, x1)) → LAST(head(cons(x0, x1)), x1) at position [0] we obtained the following new rules:
IF(false, y0, cons(x0, x1)) → LAST(x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, cons(x0, x1)) → LAST(x0, x1)
The TRS R consists of the following rules:
head(cons(x, l)) → x
The set Q consists of the following terms:
head(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, cons(x0, x1)) → LAST(x0, x1)
R is empty.
The set Q consists of the following terms:
head(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
head(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
IF(false, y0, cons(x0, x1)) → LAST(x0, x1)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- IF(false, y0, cons(x0, x1)) → LAST(x0, x1)
The graph contains the following edges 3 > 1, 3 > 2
- LAST(y0, cons(x0, x1)) → IF(false, y0, cons(x0, x1))
The graph contains the following edges 1 >= 2, 2 >= 3
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
The TRS R consists of the following rules:
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
The TRS R consists of the following rules:
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
The set Q consists of the following terms:
rev(nil)
rev(cons(x0, x1))
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
The remaining pairs can at least be oriented weakly.
REV(cons(x, l)) → REV2(x, l)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
| M( cons(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
| M( rev2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
| M( rev1(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
| M( REV2(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
rev2(x, nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
REV(cons(x, l)) → REV2(x, l)
The TRS R consists of the following rules:
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
The set Q consists of the following terms:
rev(nil)
rev(cons(x0, x1))
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.